Active Learning of Points-To Specifications

摘要

When analyzing programs, large libraries pose significant challenges tostatic points-to analysis. A popular solution is to have a human analystprovide points-to specifications that summarize relevant behaviors of librarycode, which can substantially improve precision and furthermore handle missingcode such as native code. We propose Atlas, a tool that automatically inferspoints-to specifications. Atlas synthesizes unit tests that exercise thelibrary code, and then infers points-to specifications based on observationsfrom these executions. Atlas automatically infers specifications for the Javastandard library, and produces better results for a client static informationflow analysis on a benchmark of 46 Android apps compared to using existinghandwritten specifications.